Nuprl Lemma : fpf-sub_transitivity 0,22

A:Type, B:(AType), eq:EqDecider(A), fgh:a:A fp B(a). f  g  g  h  f  h 
latex


DefinitionsEqDecider(T), f  g, b, x  dom(f), a:A fp B(a), Top, xt(x), x(s), P  Q, t  T, x:AB(x), A & B
Lemmasfpf-trivial-subtype-top, fpf-dom wf, assert wf, deq wf, fpf wf, fpf-sub wf

origin